STM: es realizer wf

ABS: Rnone()

STM: Rnone wf

ABS: left  right

STM: Rplus wf

ABS: Rinit(loc;T;x;v)

STM: Rinit wf

ABS: Rframe(loc;T;x;L)

STM: Rframe wf

ABS: Rsframe(lnk;tag;L)

STM: Rsframe wf

ABS: Reffect(loc;ds;knd;T;x;f)

STM: Reffect wf

ABS: Rsends(ds;knd;T;l;dt;g)

STM: Rsends wf

ABS: Rpre(loc;ds;a;p;P)

STM: Rpre wf

ABS: Raframe(loc;k;L)

STM: Raframe wf

ABS: Rbframe(loc;k;L)

STM: Rbframe wf

ABS: Rrframe(loc;x;L)

STM: Rrframe wf

ABS: es realizer ind

STM: es realizer ind wf

STM: es realizer-induction

ABS: es realizer ind Rnone compseq tag def

ABS: es realizer ind Rplus compseq tag def

ABS: es realizer ind Rinit compseq tag def

ABS: es realizer ind Rframe compseq tag def

ABS: es realizer ind Rsframe compseq tag def

ABS: es realizer ind Reffect compseq tag def

ABS: es realizer ind Rsends compseq tag def

ABS: es realizer ind Rpre compseq tag def

ABS: es realizer ind Raframe compseq tag def

ABS: es realizer ind Rbframe compseq tag def

ABS: es realizer ind Rrframe compseq tag def

ABS: Rnone?(x1)

STM: Rnone? wf

ABS: Rplus?(x1)

STM: Rplus? wf

ABS: Rplus-left(x1)

STM: Rplus-left wf

ABS: Rplus-right(x1)

STM: Rplus-right wf

ABS: Rinit?(x1)

STM: Rinit? wf

ABS: Rinit-loc(x1)

STM: Rinit-loc wf

ABS: Rinit-T(x1)

STM: Rinit-T wf

ABS: Rinit-x(x1)

STM: Rinit-x wf

ABS: Rinit-v(x1)

STM: Rinit-v wf

ABS: Rframe?(x1)

STM: Rframe? wf

ABS: Rframe-loc(x1)

STM: Rframe-loc wf

ABS: Rframe-T(x1)

STM: Rframe-T wf

ABS: Rframe-x(x1)

STM: Rframe-x wf

ABS: Rframe-L(x1)

STM: Rframe-L wf

ABS: Rsframe?(x1)

STM: Rsframe? wf

ABS: Rsframe-lnk(x1)

STM: Rsframe-lnk wf

ABS: Rsframe-tag(x1)

STM: Rsframe-tag wf

ABS: Rsframe-L(x1)

STM: Rsframe-L wf

ABS: Reffect?(x1)

STM: Reffect? wf

ABS: Reffect-loc(x1)

STM: Reffect-loc wf

ABS: Reffect-ds(x1)

STM: Reffect-ds wf

ABS: Reffect-knd(x1)

STM: Reffect-knd wf

ABS: Reffect-T(x1)

STM: Reffect-T wf

ABS: Reffect-x(x1)

STM: Reffect-x wf

ABS: Reffect-f(x1)

STM: Reffect-f wf

ABS: Rsends?(x1)

STM: Rsends? wf

ABS: Rsends-ds(x1)

STM: Rsends-ds wf

ABS: Rsends-knd(x1)

STM: Rsends-knd wf

ABS: Rsends-T(x1)

STM: Rsends-T wf

ABS: Rsends-l(x1)

STM: Rsends-l wf

ABS: Rsends-dt(x1)

STM: Rsends-dt wf

ABS: Rsends-g(x1)

STM: Rsends-g wf

ABS: Rpre?(x1)

STM: Rpre? wf

ABS: Rpre-loc(x1)

STM: Rpre-loc wf

ABS: Rpre-ds(x1)

STM: Rpre-ds wf

ABS: Rpre-a(x1)

STM: Rpre-a wf

ABS: Rpre-p(x1)

STM: Rpre-p wf

ABS: Rpre-P(x1)

STM: Rpre-P wf

ABS: Raframe?(x1)

STM: Raframe? wf

ABS: Raframe-loc(x1)

STM: Raframe-loc wf

ABS: Raframe-k(x1)

STM: Raframe-k wf

ABS: Raframe-L(x1)

STM: Raframe-L wf

ABS: Rbframe?(x1)

STM: Rbframe? wf

ABS: Rbframe-loc(x1)

STM: Rbframe-loc wf

ABS: Rbframe-k(x1)

STM: Rbframe-k wf

ABS: Rbframe-L(x1)

STM: Rbframe-L wf

ABS: Rrframe?(x1)

STM: Rrframe? wf

ABS: Rrframe-loc(x1)

STM: Rrframe-loc wf

ABS: Rrframe-x(x1)

STM: Rrframe-x wf

ABS: Rrframe-L(x1)

STM: Rrframe-L wf